(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_187 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EAX_5_89 () (_ BitVec 32))
(declare-fun R_EBP_0_70 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert (let ((?v_27 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_187 (bvadd R_ESP_1_58 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_187 (bvadd R_ESP_1_58 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_187 (bvadd R_ESP_1_58 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_187 (bvadd R_ESP_1_58 (_ bv3 32)))) (_ bv24 32)))) (?v_3 (bvsub R_ESP_1_58 (_ bv4 32)))) (let ((?v_5 (bvadd ?v_3 (_ bv4 32)))) (let ((?v_28 (bvadd ?v_5 (_ bv0 32))) (?v_0 (bvsub ?v_3 (_ bv4 32)))) (let ((?v_1 (store (store (store (store mem_35_187 (bvadd ?v_0 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv24 32)))) (bvadd ?v_0 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv16 32)))) (bvadd ?v_0 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv8 32)))) (bvadd ?v_0 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_70)))) (let ((?v_9 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_1 (_ bv134567760 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567761 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567762 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567763 32))) (_ bv24 32))))) (let ((?v_6 (bvand (concat (_ bv0 31) (ite (bvult ?v_9 (_ bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 32)))) (let ((?v_2 (bvand (bvsub (_ bv0 32) ?v_6) (_ bv3 32)))) (let ((?v_4 (store (store (store (store ?v_1 (_ bv134567763 32) ((_ extract 7 0) (bvlshr ?v_2 (_ bv24 32)))) (_ bv134567762 32) ((_ extract 7 0) (bvlshr ?v_2 (_ bv16 32)))) (_ bv134567761 32) ((_ extract 7 0) (bvlshr ?v_2 (_ bv8 32)))) (_ bv134567760 32) ((_ extract 7 0) ?v_2))) (?v_29 (bvadd ?v_5 (_ bv1 32))) (?v_30 (bvadd ?v_5 (_ bv2 32))) (?v_31 (bvadd ?v_5 (_ bv3 32)))) (let ((?v_20 (ite (not (= ?v_27 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_4 ?v_28)) (bvshl (concat (_ bv0 24) (select ?v_4 ?v_29)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_4 ?v_30)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_4 ?v_31)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1))) (?v_8 (bvand ?v_6 (_ bv1 32)))) (let ((?v_7 (bvxor (bvxor (_ bv0 32) ?v_6) ?v_8))) (let ((?v_21 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor (_ bv0 32) ?v_7) (bvxor (_ bv0 32) (bvsub (bvsub (_ bv0 32) ?v_7) ?v_8))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_22 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_9 (_ bv1 32)) (bvxor ?v_9 (bvsub ?v_9 (_ bv1 32)))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_10 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_1 (_ bv134567756 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567757 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567758 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134567759 32))) (_ bv24 32))))) (let ((?v_11 (bvsub ?v_9 ?v_10))) (let ((?v_23 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_11 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_24 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_9 ?v_10) (bvxor ?v_9 ?v_11)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_12 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_1 (_ bv134534684 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134534685 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134534686 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_1 (_ bv134534687 32))) (_ bv24 32))))) (let ((?v_13 (bvsub ?v_12 ?v_10))) (let ((?v_34 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_13 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_25 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) R_EAX_5_89)) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (let ((?v_40 (bvnot ?v_25)) (?v_14 (concat (_ bv0 24) (select ?v_1 (_ bv134534657 32))))) (let ((?v_15 (bvand (bvsub ?v_14 (_ bv0 32)) (_ bv255 32)))) (let ((?v_44 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_15 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_16 (concat (_ bv0 24) (select ?v_1 (_ bv134534656 32))))) (let ((?v_17 (bvand (bvsub ?v_16 (_ bv0 32)) (_ bv255 32)))) (let ((?v_41 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_17 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_18 (concat (_ bv0 24) (select mem_35_187 (_ bv134534658 32))))) (let ((?v_19 (bvand (bvsub ?v_18 (_ bv0 32)) (_ bv255 32)))) (let ((?v_48 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_19 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_49 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_18 (_ bv0 32)) (bvxor ?v_18 ?v_19)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1)))) (let ((?v_42 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_16 (_ bv0 32)) (bvxor ?v_16 ?v_17)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_48 ?v_49)))) (let ((?v_45 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_14 (_ bv0 32)) (bvxor ?v_14 ?v_15)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_41 ?v_42)))) (let ((?v_26 (bvand (bvnot ?v_44) ?v_45))) (let ((?v_35 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_12 ?v_10) (bvxor ?v_12 ?v_13)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_40 ?v_26)))) (let ((?v_32 (bvand ?v_24 (bvand ?v_34 ?v_35))) (?v_38 (bvand ?v_24 (bvand ?v_25 ?v_26))) (?v_36 (ite (not (= ?v_27 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_1 ?v_28)) (bvshl (concat (_ bv0 24) (select ?v_1 ?v_29)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_1 ?v_30)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_1 ?v_31)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1))) (?v_37 (bvnot ?v_23)) (?v_33 (store (store (store (store ?v_1 (_ bv134567763 32) ((_ extract 7 0) (bvlshr ?v_12 (_ bv24 32)))) (_ bv134567762 32) ((_ extract 7 0) (bvlshr ?v_12 (_ bv16 32)))) (_ bv134567761 32) ((_ extract 7 0) (bvlshr ?v_12 (_ bv8 32)))) (_ bv134567760 32) ((_ extract 7 0) ?v_12)))) (let ((?v_39 (ite (not (= ?v_27 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_33 ?v_28)) (bvshl (concat (_ bv0 24) (select ?v_33 ?v_29)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_33 ?v_30)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_33 ?v_31)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1))) (?v_47 (bvand (bvnot ?v_41) ?v_42)) (?v_43 (store (store (store (store ?v_1 (_ bv134567763 32) ((_ extract 7 0) (bvlshr ?v_10 (_ bv24 32)))) (_ bv134567762 32) ((_ extract 7 0) (bvlshr ?v_10 (_ bv16 32)))) (_ bv134567761 32) ((_ extract 7 0) (bvlshr ?v_10 (_ bv8 32)))) (_ bv134567760 32) ((_ extract 7 0) ?v_10)))) (let ((?v_46 (ite (not (= ?v_27 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_43 ?v_28)) (bvshl (concat (_ bv0 24) (select ?v_43 ?v_29)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_43 ?v_30)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_43 ?v_31)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)))) (= (_ bv1 1) (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvand ?v_20 (bvand ?v_21 (bvand ?v_22 (bvand ?v_23 ?v_32)))) (bvand ?v_20 (bvand ?v_21 (bvand ?v_22 (bvand ?v_23 ?v_38))))) (bvand ?v_36 (bvand ?v_37 ?v_32))) (bvand ?v_39 (bvand (bvnot ?v_34) ?v_35))) (bvand ?v_36 (bvand ?v_37 ?v_38))) (bvand ?v_39 (bvand ?v_40 ?v_47))) (bvand ?v_46 (bvand ?v_44 ?v_45))) (bvand ?v_46 (bvand ?v_25 ?v_47))) (bvand ?v_46 (bvand (bvnot ?v_48) ?v_49))))))))))))))))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
